Search Results

Documents authored by Milius, Stefan

Document
(Co)algebraic pearls
DOI: 10.4230/LIPIcs.CALCO.2023.21
On Kripke, Vietoris and Hausdorff Polynomial Functors ((Co)algebraic pearls)

Authors: Jiří Adámek, Stefan Milius, and Lawrence S. Moss

Published in: LIPIcs, Volume 270, 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)

Abstract
The Vietoris space of compact subsets of a given Hausdorff space yields an endofunctor V on the category of Hausdorff spaces. Vietoris polynomial endofunctors on that category are built from V, the identity and constant functors by forming products, coproducts and compositions. These functors are known to have terminal coalgebras and we deduce that they also have initial algebras. We present an analogous class of endofunctors on the category of extended metric spaces, using in lieu of V the Hausdorff functor ℋ. We prove that the ensuing Hausdorff polynomial functors have terminal coalgebras and initial algebras. Whereas the canonical constructions of terminal coalgebras for Vietoris polynomial functors takes ω steps, one needs ω + ω steps in general for Hausdorff ones. We also give a new proof that the closed set functor on metric spaces has no fixed points.
Cite as

Jiří Adámek, Stefan Milius, and Lawrence S. Moss. On Kripke, Vietoris and Hausdorff Polynomial Functors ((Co)algebraic pearls). In 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 270, pp. 21:1-21:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{adamek_et_al:LIPIcs.CALCO.2023.21,
  author =	{Ad\'{a}mek, Ji\v{r}{\'\i} and Milius, Stefan and Moss, Lawrence S.},
  title =	{{On Kripke, Vietoris and Hausdorff Polynomial Functors}},
  booktitle =	{10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)},
  pages =	{21:1--21:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-287-7},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{270},
  editor =	{Baldan, Paolo and de Paiva, Valeria},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2023.21},
  URN =		{urn:nbn:de:0030-drops-188189},
  doi =		{10.4230/LIPIcs.CALCO.2023.21},
  annote =	{Keywords: Hausdorff functor, Vietoris functor, initial algebra, terminal coalgebra}
}
Document
Early Ideas
DOI: 10.4230/LIPIcs.CALCO.2023.24
Higher-Order Mathematical Operational Semantics (Early Ideas)

Authors: Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas, and Henning Urbat

Published in: LIPIcs, Volume 270, 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)

Abstract
We present a higher-order extension of Turi and Plotkin’s abstract GSOS framework that retains the key feature of the latter: for every language whose operational rules are represented by a higher-order GSOS law, strong bisimilarity on the canonical operational model is a congruence with respect to the operations of the language. We further extend this result to weak (bi-)similarity, for which a categorical account of Howe’s method is developed. It encompasses, for instance, Abramsky’s classical compositionality theorem for applicative similarity in the untyped λ-calculus. In addition, we give first steps of a theory of logical relations at the level of higher-order abstract GSOS.
Cite as

Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas, and Henning Urbat. Higher-Order Mathematical Operational Semantics (Early Ideas). In 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 270, pp. 24:1-24:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{goncharov_et_al:LIPIcs.CALCO.2023.24,
  author =	{Goncharov, Sergey and Milius, Stefan and Schr\"{o}der, Lutz and Tsampas, Stelios and Urbat, Henning},
  title =	{{Higher-Order Mathematical Operational Semantics}},
  booktitle =	{10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)},
  pages =	{24:1--24:3},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-287-7},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{270},
  editor =	{Baldan, Paolo and de Paiva, Valeria},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2023.24},
  URN =		{urn:nbn:de:0030-drops-188213},
  doi =		{10.4230/LIPIcs.CALCO.2023.24},
  annote =	{Keywords: Abstract GSOS, lambda-calculus, applicative bisimilarity, bialgebra}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2023.48
Positive Data Languages

Authors: Florian Frank, Stefan Milius, and Henning Urbat

Published in: LIPIcs, Volume 272, 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)

Abstract
Positive data languages are languages over an infinite alphabet closed under possibly non-injective renamings of data values. Informally, they model properties of data words expressible by assertions about equality, but not inequality, of data values occurring in the word. We investigate the class of positive data languages recognizable by nondeterministic orbit-finite nominal automata, an abstract form of register automata introduced by Bojańczyk, Klin, and Lasota. As our main contribution we provide a number of equivalent characterizations of that class in terms of positive register automata, monadic second-order logic with positive equality tests, and finitely presentable nondeterministic automata in the categories of nominal renaming sets and of presheaves over finite sets.
Cite as

Florian Frank, Stefan Milius, and Henning Urbat. Positive Data Languages. In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 48:1-48:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{frank_et_al:LIPIcs.MFCS.2023.48,
  author =	{Frank, Florian and Milius, Stefan and Urbat, Henning},
  title =	{{Positive Data Languages}},
  booktitle =	{48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)},
  pages =	{48:1--48:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-292-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{272},
  editor =	{Leroux, J\'{e}r\^{o}me and Lombardy, Sylvain and Peleg, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2023.48},
  URN =		{urn:nbn:de:0030-drops-185828},
  doi =		{10.4230/LIPIcs.MFCS.2023.48},
  annote =	{Keywords: Data Languages, Register Automata, MSO, Nominal Sets, Presheaves}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2023.114
Nominal Topology for Data Languages

Authors: Fabian Birkmann, Stefan Milius, and Henning Urbat

Published in: LIPIcs, Volume 261, 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)

Abstract
We propose a novel topological perspective on data languages recognizable by orbit-finite nominal monoids. For this purpose, we introduce pro-orbit-finite nominal topological spaces. Assuming globally bounded support sizes, they coincide with nominal Stone spaces and are shown to be dually equivalent to a subcategory of nominal boolean algebras. Recognizable data languages are characterized as topologically clopen sets of pro-orbit-finite words. In addition, we explore the expressive power of pro-orbit-finite equations by establishing a nominal version of Reiterman’s pseudovariety theorem.
Cite as

Fabian Birkmann, Stefan Milius, and Henning Urbat. Nominal Topology for Data Languages. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 114:1-114:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{birkmann_et_al:LIPIcs.ICALP.2023.114,
  author =	{Birkmann, Fabian and Milius, Stefan and Urbat, Henning},
  title =	{{Nominal Topology for Data Languages}},
  booktitle =	{50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)},
  pages =	{114:1--114:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-278-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{261},
  editor =	{Etessami, Kousha and Feige, Uriel and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2023.114},
  URN =		{urn:nbn:de:0030-drops-181662},
  doi =		{10.4230/LIPIcs.ICALP.2023.114},
  annote =	{Keywords: Nominal sets, Stone duality, Profinite space, Data languages}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2022.30
Stateful Structural Operational Semantics

Authors: Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas, and Henning Urbat

Published in: LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)

Abstract
Compositionality of denotational semantics is an important concern in programming semantics. Mathematical operational semantics in the sense of Turi and Plotkin guarantees compositionality, but seen from the point of view of stateful computation it applies only to very fine-grained equivalences that essentially assume unrestricted interference by the environment between any two statements. We introduce the more restrictive stateful SOS rule format for stateful languages. We show that compositionality of two more coarse-grained semantics, respectively given by assuming read-only interference or no interference between steps, remains an undecidable property even for stateful SOS. However, further restricting the rule format in a manner inspired by the cool GSOS formats of Bloom and van Glabbeek, we obtain the streamlined and cool stateful SOS formats, which respectively guarantee compositionality of the two more abstract equivalences.
Cite as

Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas, and Henning Urbat. Stateful Structural Operational Semantics. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 30:1-30:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{goncharov_et_al:LIPIcs.FSCD.2022.30,
  author =	{Goncharov, Sergey and Milius, Stefan and Schr\"{o}der, Lutz and Tsampas, Stelios and Urbat, Henning},
  title =	{{Stateful Structural Operational Semantics}},
  booktitle =	{7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
  pages =	{30:1--30:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-233-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{228},
  editor =	{Felty, Amy P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.30},
  URN =		{urn:nbn:de:0030-drops-163111},
  doi =		{10.4230/LIPIcs.FSCD.2022.30},
  annote =	{Keywords: Structural Operational Semantics, Rule Formats, Distributive Laws}
}
Document
(Co)algebraic pearls
DOI: 10.4230/LIPIcs.CALCO.2021.5
Initial Algebras Without Iteration ((Co)algebraic pearls)

Authors: Jiří Adámek, Stefan Milius, and Lawrence S. Moss

Published in: LIPIcs, Volume 211, 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)

Abstract
The Initial Algebra Theorem by Trnková et al. states, under mild assumptions, that an endofunctor has an initial algebra provided it has a pre-fixed point. The proof crucially depends on transfinitely iterating the functor and in fact shows that, equivalently, the (transfinite) initial-algebra chain stops. We give a constructive proof of the Initial Algebra Theorem that avoids transfinite iteration of the functor. For a given pre-fixed point A of the functor, it uses Pataraia’s theorem to obtain the least fixed point of a monotone function on the partial order formed by all subobjects of A. Thanks to properties of recursive coalgebras, this least fixed point yields an initial algebra. We obtain new results on fixed points and initial algebras in categories enriched over directed-complete partial orders, again without iteration. Using transfinite iteration we equivalently obtain convergence of the initial-algebra chain as an equivalent condition, overall yielding a streamlined version of the original proof.
Cite as

Jiří Adámek, Stefan Milius, and Lawrence S. Moss. Initial Algebras Without Iteration ((Co)algebraic pearls). In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 5:1-5:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{adamek_et_al:LIPIcs.CALCO.2021.5,
  author =	{Ad\'{a}mek, Ji\v{r}{\'\i} and Milius, Stefan and Moss, Lawrence S.},
  title =	{{Initial Algebras Without Iteration}},
  booktitle =	{9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)},
  pages =	{5:1--5:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-212-9},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{211},
  editor =	{Gadducci, Fabio and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.5},
  URN =		{urn:nbn:de:0030-drops-153606},
  doi =		{10.4230/LIPIcs.CALCO.2021.5},
  annote =	{Keywords: Initial algebra, Pataraia’s theorem, recursive coalgebra, initial-algebra chain}
}
Document
DOI: 10.4230/LIPIcs.CALCO.2021.14
Monads on Categories of Relational Structures

Authors: Chase Ford, Stefan Milius, and Lutz Schröder

Published in: LIPIcs, Volume 211, 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)

Abstract
We introduce a framework for universal algebra in categories of relational structures given by finitary relational signatures and finitary or infinitary Horn theories, with the arity λ of a Horn theory understood as a strict upper bound on the number of premisses in its axioms; key examples include partial orders (λ = ω) or metric spaces (λ = ω₁). We establish a bijective correspondence between λ-accessible enriched monads on the given category of relational structures and a notion of λ-ary algebraic theories (i.e. with operations of arity < λ), with the syntax of algebraic theories induced by the relational signature (e.g. inequations or equations-up-to-ε). We provide a generic sound and complete derivation system for such relational algebraic theories, thus in particular recovering (extensions of) recent systems of this type for monads on partial orders and metric spaces by instantiation. In particular, we present an ω₁-ary algebraic theory of metric completion. The theory-to-monad direction of our correspondence remains true for the case of κ-ary algebraic theories and κ-accessible monads for κ < λ, e.g. for finitary theories over metric spaces.
Cite as

Chase Ford, Stefan Milius, and Lutz Schröder. Monads on Categories of Relational Structures. In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 14:1-14:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{ford_et_al:LIPIcs.CALCO.2021.14,
  author =	{Ford, Chase and Milius, Stefan and Schr\"{o}der, Lutz},
  title =	{{Monads on Categories of Relational Structures}},
  booktitle =	{9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)},
  pages =	{14:1--14:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-212-9},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{211},
  editor =	{Gadducci, Fabio and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.14},
  URN =		{urn:nbn:de:0030-drops-153697},
  doi =		{10.4230/LIPIcs.CALCO.2021.14},
  annote =	{Keywords: monads, relational structures, Horn theories, relational logic}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2021.58
A Linear-Time Nominal μ-Calculus with Name Allocation

Authors: Daniel Hausmann, Stefan Milius, and Lutz Schröder

Published in: LIPIcs, Volume 202, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)

Abstract
Logics and automata models for languages over infinite alphabets, such as Freeze LTL and register automata, serve the verification of processes or documents with data. They relate tightly to formalisms over nominal sets, such as nondetermininistic orbit-finite automata (NOFAs), where names play the role of data. Reasoning problems in such formalisms tend to be computationally hard. Name-binding nominal automata models such as {regular nondeterministic nominal automata (RNNAs)} have been shown to be computationally more tractable. In the present paper, we introduce a linear-time fixpoint logic Bar-μTL} for finite words over an infinite alphabet, which features full negation and freeze quantification via name binding. We show by a nontrivial reduction to extended regular nondeterministic nominal automata that even though Bar-μTL} allows unrestricted nondeterminism and unboundedly many registers, model checking Bar-μTL} over RNNAs and satisfiability checking both have elementary complexity. For example, model checking is in 2ExpSpace, more precisely in parametrized ExpSpace, effectively with the number of registers as the parameter.
Cite as

Daniel Hausmann, Stefan Milius, and Lutz Schröder. A Linear-Time Nominal μ-Calculus with Name Allocation. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 58:1-58:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{hausmann_et_al:LIPIcs.MFCS.2021.58,
  author =	{Hausmann, Daniel and Milius, Stefan and Schr\"{o}der, Lutz},
  title =	{{A Linear-Time Nominal \mu-Calculus with Name Allocation}},
  booktitle =	{46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)},
  pages =	{58:1--58:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-201-3},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{202},
  editor =	{Bonchi, Filippo and Puglisi, Simon J.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2021.58},
  URN =		{urn:nbn:de:0030-drops-144987},
  doi =		{10.4230/LIPIcs.MFCS.2021.58},
  annote =	{Keywords: Model checking, linear-time logic, nominal sets}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2021.4
Nominal Büchi Automata with Name Allocation

Authors: Henning Urbat, Daniel Hausmann, Stefan Milius, and Lutz Schröder

Published in: LIPIcs, Volume 203, 32nd International Conference on Concurrency Theory (CONCUR 2021)

Abstract
Infinite words over infinite alphabets serve as models of the temporal development of the allocation and (re-)use of resources over linear time. We approach ω-languages over infinite alphabets in the setting of nominal sets, and study languages of infinite bar strings, i.e. infinite sequences of names that feature binding of fresh names; binding corresponds roughly to reading letters from input words in automata models with registers. We introduce regular nominal nondeterministic Büchi automata (Büchi RNNAs), an automata model for languages of infinite bar strings, repurposing the previously introduced RNNAs over finite bar strings. Our machines feature explicit binding (i.e. resource-allocating) transitions and process their input via a Büchi-type acceptance condition. They emerge from the abstract perspective on name binding given by the theory of nominal sets. As our main result we prove that, in contrast to most other nondeterministic automata models over infinite alphabets, language inclusion of Büchi RNNAs is decidable and in fact elementary. This makes Büchi RNNAs a suitable tool for applications in model checking.
Cite as

Henning Urbat, Daniel Hausmann, Stefan Milius, and Lutz Schröder. Nominal Büchi Automata with Name Allocation. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 4:1-4:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{urbat_et_al:LIPIcs.CONCUR.2021.4,
  author =	{Urbat, Henning and Hausmann, Daniel and Milius, Stefan and Schr\"{o}der, Lutz},
  title =	{{Nominal B\"{u}chi Automata with Name Allocation}},
  booktitle =	{32nd International Conference on Concurrency Theory (CONCUR 2021)},
  pages =	{4:1--4:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-203-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{203},
  editor =	{Haddad, Serge and Varacca, Daniele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.4},
  URN =		{urn:nbn:de:0030-drops-143813},
  doi =		{10.4230/LIPIcs.CONCUR.2021.4},
  annote =	{Keywords: Data languages, infinite words, nominal sets, inclusion checking}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2021.32
Explaining Behavioural Inequivalence Generically in Quasilinear Time

Authors: Thorsten Wißmann, Stefan Milius, and Lutz Schröder

Published in: LIPIcs, Volume 203, 32nd International Conference on Concurrency Theory (CONCUR 2021)

Abstract
We provide a generic algorithm for constructing formulae that distinguish behaviourally inequivalent states in systems of various transition types such as nondeterministic, probabilistic or weighted; genericity over the transition type is achieved by working with coalgebras for a set functor in the paradigm of universal coalgebra. For every behavioural equivalence class in a given system, we construct a formula which holds precisely at the states in that class. The algorithm instantiates to deterministic finite automata, transition systems, labelled Markov chains, and systems of many other types. The ambient logic is a modal logic featuring modalities that are generically extracted from the functor; these modalities can be systematically translated into custom sets of modalities in a postprocessing step. The new algorithm builds on an existing coalgebraic partition refinement algorithm. It runs in time 𝒪((m+n) log n) on systems with n states and m transitions, and the same asymptotic bound applies to the dag size of the formulae it constructs. This improves the bounds on run time and formula size compared to previous algorithms even for previously known specific instances, viz. transition systems and Markov chains; in particular, the best previous bound for transition systems was 𝒪(m n).
Cite as

Thorsten Wißmann, Stefan Milius, and Lutz Schröder. Explaining Behavioural Inequivalence Generically in Quasilinear Time. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 32:1-32:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{wimann_et_al:LIPIcs.CONCUR.2021.32,
  author =	{Wi{\ss}mann, Thorsten and Milius, Stefan and Schr\"{o}der, Lutz},
  title =	{{Explaining Behavioural Inequivalence Generically in Quasilinear Time}},
  booktitle =	{32nd International Conference on Concurrency Theory (CONCUR 2021)},
  pages =	{32:1--32:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-203-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{203},
  editor =	{Haddad, Serge and Varacca, Daniele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.32},
  URN =		{urn:nbn:de:0030-drops-144094},
  doi =		{10.4230/LIPIcs.CONCUR.2021.32},
  annote =	{Keywords: bisimulation, partition refinement, modal logic, distinguishing formulae, coalgebra}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2021.28
Coalgebra Encoding for Efficient Minimization

Authors: Hans-Peter Deifel, Stefan Milius, and Thorsten Wißmann

Published in: LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)

Abstract
Recently, we have developed an efficient generic partition refinement algorithm, which computes behavioural equivalence on a state-based system given as an encoded coalgebra, and implemented it in the tool CoPaR. Here we extend this to a fully fledged minimization algorithm and tool by integrating two new aspects: (1) the computation of the transition structure on the minimized state set, and (2) the computation of the reachable part of the given system. In our generic coalgebraic setting these two aspects turn out to be surprisingly non-trivial requiring us to extend the previous theory. In particular, we identify a sufficient condition on encodings of coalgebras, and we show how to augment the existing interface, which encapsulates computations that are specific for the coalgebraic type functor, to make the above extensions possible. Both extensions have linear run time.
Cite as

Hans-Peter Deifel, Stefan Milius, and Thorsten Wißmann. Coalgebra Encoding for Efficient Minimization. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 28:1-28:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{deifel_et_al:LIPIcs.FSCD.2021.28,
  author =	{Deifel, Hans-Peter and Milius, Stefan and Wi{\ss}mann, Thorsten},
  title =	{{Coalgebra Encoding for Efficient Minimization}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{28:1--28:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-191-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{195},
  editor =	{Kobayashi, Naoki},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.28},
  URN =		{urn:nbn:de:0030-drops-142664},
  doi =		{10.4230/LIPIcs.FSCD.2021.28},
  annote =	{Keywords: Coalgebra, Partition refinement, Transition systems, Minimization}
}
Document
Invited Paper
DOI: 10.4230/LIPIcs.CALCO.2019.2
From Equational Specifications of Algebras with Structure to Varieties of Data Languages (Invited Paper)

Authors: Stefan Milius

Published in: LIPIcs, Volume 139, 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)

Abstract
This extended abstract first presents a new category theoretic approach to equationally axiomatizable classes of algebras. This approach is well-suited for the treatment of algebras equipped with additional computationally relevant structure, such as ordered algebras, continuous algebras, quantitative algebras, nominal algebras, or profinite algebras. We present a generic HSP theorem and a sound and complete equational logic, which encompass numerous flavors of equational axiomizations studied in the literature. In addition, we use the generic HSP theorem as a key ingredient to obtain Eilenberg-type correspondences yielding algebraic characterizations of properties of regular machine behaviours. When instantiated for orbit-finite nominal monoids, the generic HSP theorem yields a crucial step for the proof of the first Eilenberg-type variety theorem for data languages.
Cite as

Stefan Milius. From Equational Specifications of Algebras with Structure to Varieties of Data Languages (Invited Paper). In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 2:1-2:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{milius:LIPIcs.CALCO.2019.2,
  author =	{Milius, Stefan},
  title =	{{From Equational Specifications of Algebras with Structure to Varieties of Data Languages}},
  booktitle =	{8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
  pages =	{2:1--2:5},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-120-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{139},
  editor =	{Roggenbach, Markus and Sokolova, Ana},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.2},
  URN =		{urn:nbn:de:0030-drops-114309},
  doi =		{10.4230/LIPIcs.CALCO.2019.2},
  annote =	{Keywords: Birkhoff theorem, Equational logic, Eilenberg theorem, Data languages}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2019.36
Graded Monads and Graded Logics for the Linear Time - Branching Time Spectrum

Authors: Ulrich Dorsch, Stefan Milius, and Lutz Schröder

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)

Abstract
State-based models of concurrent systems are traditionally considered under a variety of notions of process equivalence. In the case of labelled transition systems, these equivalences range from trace equivalence to (strong) bisimilarity, and are organized in what is known as the linear time - branching time spectrum. A combination of universal coalgebra and graded monads provides a generic framework in which the semantics of concurrency can be parametrized both over the branching type of the underlying transition systems and over the granularity of process equivalence. We show in the present paper that this framework of graded semantics does subsume the most important equivalences from the linear time - branching time spectrum. An important feature of graded semantics is that it allows for the principled extraction of characteristic modal logics. We have established invariance of these graded logics under the given graded semantics in earlier work; in the present paper, we extend the logical framework with an explicit propositional layer and provide a generic expressiveness criterion that generalizes the classical Hennessy-Milner theorem to coarser notions of process equivalence. We extract graded logics for a range of graded semantics on labelled transition systems and probabilistic systems, and give exemplary proofs of their expressiveness based on our generic criterion.
Cite as

Ulrich Dorsch, Stefan Milius, and Lutz Schröder. Graded Monads and Graded Logics for the Linear Time - Branching Time Spectrum. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 36:1-36:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{dorsch_et_al:LIPIcs.CONCUR.2019.36,
  author =	{Dorsch, Ulrich and Milius, Stefan and Schr\"{o}der, Lutz},
  title =	{{Graded Monads and Graded Logics for the Linear Time - Branching Time Spectrum}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{36:1--36:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.36},
  URN =		{urn:nbn:de:0030-drops-109384},
  doi =		{10.4230/LIPIcs.CONCUR.2019.36},
  annote =	{Keywords: Linear Time, Branching Time, Monads, System Equivalences, Modal Logics, Expressiveness}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2019.130
Varieties of Data Languages (Track B: Automata, Logic, Semantics, and Theory of Programming)

Authors: Henning Urbat and Stefan Milius

Published in: LIPIcs, Volume 132, 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)

Abstract
We establish an Eilenberg-type correspondence for data languages, i.e. languages over an infinite alphabet. More precisely, we prove that there is a bijective correspondence between varieties of languages recognized by orbit-finite nominal monoids and pseudovarieties of such monoids. This is the first result of this kind for data languages. Our approach makes use of nominal Stone duality and a recent category theoretic generalization of Birkhoff-type theorems that we instantiate here for the category of nominal sets. In addition, we prove an axiomatic characterization of weak pseudovarieties as those classes of orbit-finite monoids that can be specified by sequences of nominal equations, which provides a nominal version of a classical theorem of Eilenberg and Schützenberger.
Cite as

Henning Urbat and Stefan Milius. Varieties of Data Languages (Track B: Automata, Logic, Semantics, and Theory of Programming). In 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 132, pp. 130:1-130:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{urbat_et_al:LIPIcs.ICALP.2019.130,
  author =	{Urbat, Henning and Milius, Stefan},
  title =	{{Varieties of Data Languages}},
  booktitle =	{46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)},
  pages =	{130:1--130:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-109-2},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{132},
  editor =	{Baier, Christel and Chatzigiannakis, Ioannis and Flocchini, Paola and Leonardi, Stefano},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2019.130},
  URN =		{urn:nbn:de:0030-drops-107063},
  doi =		{10.4230/LIPIcs.ICALP.2019.130},
  annote =	{Keywords: Nominal sets, Stone duality, Algebraic language theory, Data languages}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2017.43
Eilenberg Theorems for Free

Authors: Henning Urbat, Jiri Adámek, Liang-Ting Chen, and Stefan Milius

Published in: LIPIcs, Volume 83, 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)

Abstract
Eilenberg-type correspondences, relating varieties of languages (e.g., of finite words, infinite words, or trees) to pseudovarieties of finite algebras, form the backbone of algebraic language theory. We show that they all arise from the same recipe: one models languages and the algebras recognizing them by monads on an algebraic category, and applies a Stone-type duality. Our main contribution is a variety theorem that covers e.g. Wilke's and Pin's work on infinity-languages, the variety theorem for cost functions of Daviaud, Kuperberg, and Pin, and unifies the two categorical approaches of Bojanczyk and of Adamek et al. In addition we derive new results, such as an extension of the local variety theorem of Gehrke, Grigorieff, and Pin from finite to infinite words.
Cite as

Henning Urbat, Jiri Adámek, Liang-Ting Chen, and Stefan Milius. Eilenberg Theorems for Free. In 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 83, pp. 43:1-43:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{urbat_et_al:LIPIcs.MFCS.2017.43,
  author =	{Urbat, Henning and Ad\'{a}mek, Jiri and Chen, Liang-Ting and Milius, Stefan},
  title =	{{Eilenberg Theorems for Free}},
  booktitle =	{42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)},
  pages =	{43:1--43:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-046-0},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{83},
  editor =	{Larsen, Kim G. and Bodlaender, Hans L. and Raskin, Jean-Francois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2017.43},
  URN =		{urn:nbn:de:0030-drops-81032},
  doi =		{10.4230/LIPIcs.MFCS.2017.43},
  annote =	{Keywords: Eilenberg's theorem, variety of languages, pseudovariety, monad, duality}
}
Document
DOI: 10.4230/LIPIcs.CALCO.2017.3
On Corecursive Algebras for Functors Preserving Coproducts

Authors: Jiri Adámek and Stefan Milius

Published in: LIPIcs, Volume 72, 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)

Abstract
For an endofunctor H on a hyper-extensive category preserving countable coproducts we describe the free corecursive algebra on Y as the coproduct of the terminal coalgebra for H and the free H-algebra on Y. As a consequence, we derive that H is a cia functor, i.e., its corecursive algebras are precisely the cias (completely iterative algebras). Also all functors H(-) + Y are then cia functors. For finitary set functors we prove that, conversely, if H is a cia functor, then it has the form H = W \times (-) + Y for some sets W and Y.
Cite as

Jiri Adámek and Stefan Milius. On Corecursive Algebras for Functors Preserving Coproducts. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 3:1-3:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{adamek_et_al:LIPIcs.CALCO.2017.3,
  author =	{Ad\'{a}mek, Jiri and Milius, Stefan},
  title =	{{On Corecursive Algebras for Functors Preserving Coproducts}},
  booktitle =	{7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)},
  pages =	{3:1--3:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-033-0},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{72},
  editor =	{Bonchi, Filippo and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2017.3},
  URN =		{urn:nbn:de:0030-drops-80298},
  doi =		{10.4230/LIPIcs.CALCO.2017.3},
  annote =	{Keywords: terminal coalgebra, free algebra, corecursive algebra, hyper-extensive category}
}
Document
DOI: 10.4230/LIPIcs.CALCO.2017.18
Proper Functors and their Rational Fixed Point

Authors: Stefan Milius

Published in: LIPIcs, Volume 72, 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)

Abstract
The rational fixed point of a set functor is well-known to capture the behaviour of finite coalgebras. In this paper we consider functors on algebraic categories. For them the rational fixed point may no longer be a subcoalgebra of the final coalgebra. Inspired by Ésik and Maletti's notion of proper semiring, we introduce the notion of a proper functor. We show that for proper functors the rational fixed point is determined as the colimit of all coalgebras with a free finitely generated algebra as carrier and it is a subcoalgebra of the final coalgebra. Moreover, we prove that a functor is proper if and only if that colimit is a subcoalgebra of the final coalgebra. These results serve as technical tools for soundness and completeness proofs for coalgebraic regular expression calculi, e.g. for weighted automata.
Cite as

Stefan Milius. Proper Functors and their Rational Fixed Point. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 18:1-18:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{milius:LIPIcs.CALCO.2017.18,
  author =	{Milius, Stefan},
  title =	{{Proper Functors and their Rational Fixed Point}},
  booktitle =	{7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)},
  pages =	{18:1--18:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-033-0},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{72},
  editor =	{Bonchi, Filippo and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2017.18},
  URN =		{urn:nbn:de:0030-drops-80314},
  doi =		{10.4230/LIPIcs.CALCO.2017.18},
  annote =	{Keywords: proper functor, proper semiring, coalgebra, rational fixed point}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2017.32
Efficient Coalgebraic Partition Refinement

Authors: Ulrich Dorsch, Stefan Milius, Lutz Schröder, and Thorsten Wißmann

Published in: LIPIcs, Volume 85, 28th International Conference on Concurrency Theory (CONCUR 2017)

Abstract
We present a generic partition refinement algorithm that quotients coalgebraic systems by behavioural equivalence, an important task in reactive verification; coalgebraic generality implies in particular that we cover not only classical relational systems but also various forms of weighted systems. Under assumptions on the type functor that allow representing its finite coalgebras in terms of nodes and edges, our algorithm runs in time O(m log n) where n and m are the numbers of nodes and edges, respectively. Instances of our generic algorithm thus match the runtime of the best known algorithms for unlabelled transition systems, Markov chains, and deterministic automata (with fixed alphabets), and improve the best known algorithms for Segala systems.
Cite as

Ulrich Dorsch, Stefan Milius, Lutz Schröder, and Thorsten Wißmann. Efficient Coalgebraic Partition Refinement. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 32:1-32:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{dorsch_et_al:LIPIcs.CONCUR.2017.32,
  author =	{Dorsch, Ulrich and Milius, Stefan and Schr\"{o}der, Lutz and Wi{\ss}mann, Thorsten},
  title =	{{Efficient Coalgebraic Partition Refinement}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{32:1--32:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-048-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{85},
  editor =	{Meyer, Roland and Nestmann, Uwe},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.32},
  URN =		{urn:nbn:de:0030-drops-77939},
  doi =		{10.4230/LIPIcs.CONCUR.2017.32},
  annote =	{Keywords: markov chains, deterministic finite automata, partition refinement, generic algorithm, paige-tarjan algorithm, transition systems}
}
Document
DOI: 10.4230/LIPIcs.CALCO.2015.1
Syntactic Monoids in a Category

Authors: Jiri Adamek, Stefan Milius, and Henning Urbat

Published in: LIPIcs, Volume 35, 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)

Abstract
The syntactic monoid of a language is generalized to the level of a symmetric monoidal closed category D. This allows for a uniform treatment of several notions of syntactic algebras known in the literature, including the syntactic monoids of Rabin and Scott (D = sets), the syntactic semirings of Polák (D = semilattices), and the syntactic associative algebras of Reutenauer (D = vector spaces). Assuming that D is a commutative variety of algebras, we prove that the syntactic D-monoid of a language L can be constructed as a quotient of a free D-monoid modulo the syntactic congruence of L, and that it is isomorphic to the transition D-monoid of the minimal automaton for L in D. Furthermore, in the case where the variety D is locally finite, we characterize the regular languages as precisely the languages with finite syntactic D-monoids.
Cite as

Jiri Adamek, Stefan Milius, and Henning Urbat. Syntactic Monoids in a Category. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, pp. 1-16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{adamek_et_al:LIPIcs.CALCO.2015.1,
  author =	{Adamek, Jiri and Milius, Stefan and Urbat, Henning},
  title =	{{Syntactic Monoids in a Category}},
  booktitle =	{6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)},
  pages =	{1--16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-84-2},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{35},
  editor =	{Moss, Lawrence S. and Sobocinski, Pawel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2015.1},
  URN =		{urn:nbn:de:0030-drops-55235},
  doi =		{10.4230/LIPIcs.CALCO.2015.1},
  annote =	{Keywords: Syntactic monoid, transition monoid, algebraic automata theory, duality, coalgebra, algebra, symmetric monoidal closed category, commutative variety}
}
Document
DOI: 10.4230/LIPIcs.CALCO.2015.253
Generic Trace Semantics and Graded Monads

Authors: Stefan Milius, Dirk Pattinson, and Lutz Schröder

Published in: LIPIcs, Volume 35, 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)

Abstract
Models of concurrent systems employ a wide variety of semantics inducing various notions of process equivalence, ranging from linear-time semantics such as trace equivalence to branching-time semantics such as strong bisimilarity. Many of these generalize to system types beyond standard transition systems, featuring, for example, weighted, probabilistic, or game-based transitions; this motivates the search for suitable coalgebraic abstractions of process equivalence that cover these orthogonal dimensions of generality, i.e. are generic both in the system type and in the notion of system equivalence. In recent joint work with Kurz, we have proposed a parametrization of system equivalence over an embedding of the coalgebraic type functor into a monad. In the present paper, we refine this abstraction to use graded monads, which come with a notion of depth that corresponds, e.g., to trace length or bisimulation depth. We introduce a notion of graded algebras and show how they play the role of formulas in trace logics.
Cite as

Stefan Milius, Dirk Pattinson, and Lutz Schröder. Generic Trace Semantics and Graded Monads. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, pp. 253-269, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{milius_et_al:LIPIcs.CALCO.2015.253,
  author =	{Milius, Stefan and Pattinson, Dirk and Schr\"{o}der, Lutz},
  title =	{{Generic Trace Semantics and Graded Monads}},
  booktitle =	{6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)},
  pages =	{253--269},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-84-2},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{35},
  editor =	{Moss, Lawrence S. and Sobocinski, Pawel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2015.253},
  URN =		{urn:nbn:de:0030-drops-55389},
  doi =		{10.4230/LIPIcs.CALCO.2015.253},
  annote =	{Keywords: transition systems, monads, coalgebra, trace logics}
}
Document
DOI: 10.4230/LIPIcs.CALCO.2015.336
Finitary Corecursion for the Infinitary Lambda Calculus

Authors: Stefan Milius and Thorsten Wißmann

Published in: LIPIcs, Volume 35, 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)

Abstract
Kurz et al. have recently shown that infinite lambda-trees with finitely many free variables modulo alpha-equivalence form a final coalgebra for a functor on the category of nominal sets. Here we investigate the rational fixpoint of that functor. We prove that it is formed by all rational lambda-trees, i.e. those lambda-trees which have only finitely many subtrees (up to isomorphism). This yields a corecursion principle that allows the definition of operations such as substitution on rational lambda-trees.
Cite as

Stefan Milius and Thorsten Wißmann. Finitary Corecursion for the Infinitary Lambda Calculus. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, pp. 336-351, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{milius_et_al:LIPIcs.CALCO.2015.336,
  author =	{Milius, Stefan and Wi{\ss}mann, Thorsten},
  title =	{{Finitary Corecursion for the Infinitary Lambda Calculus}},
  booktitle =	{6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)},
  pages =	{336--351},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-84-2},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{35},
  editor =	{Moss, Lawrence S. and Sobocinski, Pawel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2015.336},
  URN =		{urn:nbn:de:0030-drops-55436},
  doi =		{10.4230/LIPIcs.CALCO.2015.336},
  annote =	{Keywords: rational trees, infinitary lambda calculus, coinduction}
}
Document
DOI: 10.4230/LIPIcs.CSL.2011.5
Power-Set Functors and Saturated Trees

Authors: Jiri Adamek, Stefan Milius, Lawrence S. Moss, and Lurdes Sousa

Published in: LIPIcs, Volume 12, Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL (2011)

Abstract
We combine ideas coming from several fields, including modal logic, coalgebra, and set theory. Modally saturated trees were introduced by K. Fine in 1975. We give a new purely combinatorial formulation of modally saturated trees, and we prove that they form the limit of the final omega-op-chain of the finite power-set functor Pf. From that, we derive an alternative proof of J. Worrell's description of the final coalgebra as the coalgebra of all strongly extensional, finitely branching trees. In the other direction, we represent the final coalgebra for Pf in terms of certain maximal consistent sets in the modal logic K. We also generalize Worrell's result to M-labeled trees for a commutative monoid M, yielding a final coalgebra for the corresponding functor Mf studied by H. P. Gumm and T. Schröder. We introduce the concept of an i-saturated tree for all ordinals i, and then prove that the i-th step in the final chain of the power set functor consists of all i-saturated trees. This leads to a new description of the final coalgebra for the restricted power-set functors Plambda (of subsets of cardinality smaller than lambda).
Cite as

Jiri Adamek, Stefan Milius, Lawrence S. Moss, and Lurdes Sousa. Power-Set Functors and Saturated Trees. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 5-19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{adamek_et_al:LIPIcs.CSL.2011.5,
  author =	{Adamek, Jiri and Milius, Stefan and Moss, Lawrence S. and Sousa, Lurdes},
  title =	{{Power-Set Functors and Saturated  Trees}},
  booktitle =	{Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
  pages =	{5--19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-32-3},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{12},
  editor =	{Bezem, Marc},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.5},
  URN =		{urn:nbn:de:0030-drops-32194},
  doi =		{10.4230/LIPIcs.CSL.2011.5},
  annote =	{Keywords: saturated tree, extensional tree, final coalgebra, power-set functor, modal logic}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact